A, B:Realizer. R-icompat(Rinterface(A);Rinterface(B))  R-icompat(A;B) 

latex

Definitions

p  q, let x = a in b(x), Rinterface(A), {T}, SQType(T), tt, ff, Rsends-T(x1), Rsends-knd(x1), Reffect-T(x1), Rsends-dt(x1), Rsends-l(x1), Reffect-knd(x1), Reffect?(x1), Rsends?(x1), R-interface-compat(A;B), R-loc(R), True, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), P & Q, Rplus?(x1), if b then t else f fi , Y, t  T, x. t(x), , R-icompat(A;B), P  Q, x:A. B(x), False, A, A c B, P  Q, P  Q, Unit, , x(s),

Lemmas

tagof wf, id-deq wf, fpf-cap wf, lnk wf, eq lnk wf, true wf, isrcv wf, ifthenelse wf, Rnone-implies, bool sq, bool cases, Rnone? wf, not functionality wrt iff, assert of bnot, eqff to assert, assert-eq-id, eqtt to assert, iff transitivity, lsrc wf, not wf, bnot wf, assert wf, eq id wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, rationals wf, Rinit wf, finite-prob-space wf, bool wf, Id wf, fpf wf, decl-type wf, decl-state wf, IdLnk wf, Knd wf, Rplus wf, Rnone wf, Rnone-icompat, Rinterface wf, R-icompat wf, es realizer wf, es realizer-induction